(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__fst(0, Z) → nil
a__fst(s(X), cons(Y, Z)) → cons(mark(Y), fst(X, Z))
a__from(X) → cons(mark(X), from(s(X)))
a__add(0, X) → mark(X)
a__add(s(X), Y) → s(add(X, Y))
a__len(nil) → 0
a__len(cons(X, Z)) → s(len(Z))
mark(fst(X1, X2)) → a__fst(mark(X1), mark(X2))
mark(from(X)) → a__from(mark(X))
mark(add(X1, X2)) → a__add(mark(X1), mark(X2))
mark(len(X)) → a__len(mark(X))
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__fst(X1, X2) → fst(X1, X2)
a__from(X) → from(X)
a__add(X1, X2) → add(X1, X2)
a__len(X) → len(X)
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
mark(fst(from(X28913_3), X2)) →+ a__fst(cons(mark(mark(X28913_3)), from(s(mark(X28913_3)))), mark(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [X28913_3 / fst(from(X28913_3), X2)].
The result substitution is [ ].
The rewrite sequence
mark(fst(from(X28913_3), X2)) →+ a__fst(cons(mark(mark(X28913_3)), from(s(mark(X28913_3)))), mark(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0].
The pumping substitution is [X28913_3 / fst(from(X28913_3), X2)].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__fst(0', Z) → nil
a__fst(s(X), cons(Y, Z)) → cons(mark(Y), fst(X, Z))
a__from(X) → cons(mark(X), from(s(X)))
a__add(0', X) → mark(X)
a__add(s(X), Y) → s(add(X, Y))
a__len(nil) → 0'
a__len(cons(X, Z)) → s(len(Z))
mark(fst(X1, X2)) → a__fst(mark(X1), mark(X2))
mark(from(X)) → a__from(mark(X))
mark(add(X1, X2)) → a__add(mark(X1), mark(X2))
mark(len(X)) → a__len(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__fst(X1, X2) → fst(X1, X2)
a__from(X) → from(X)
a__add(X1, X2) → add(X1, X2)
a__len(X) → len(X)
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
a__fst(0', Z) → nil
a__fst(s(X), cons(Y, Z)) → cons(mark(Y), fst(X, Z))
a__from(X) → cons(mark(X), from(s(X)))
a__add(0', X) → mark(X)
a__add(s(X), Y) → s(add(X, Y))
a__len(nil) → 0'
a__len(cons(X, Z)) → s(len(Z))
mark(fst(X1, X2)) → a__fst(mark(X1), mark(X2))
mark(from(X)) → a__from(mark(X))
mark(add(X1, X2)) → a__add(mark(X1), mark(X2))
mark(len(X)) → a__len(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__fst(X1, X2) → fst(X1, X2)
a__from(X) → from(X)
a__add(X1, X2) → add(X1, X2)
a__len(X) → len(X)
Types:
a__fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
0' :: 0':nil:s:cons:fst:from:add:len
nil :: 0':nil:s:cons:fst:from:add:len
s :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
cons :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
mark :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
hole_0':nil:s:cons:fst:from:add:len1_0 :: 0':nil:s:cons:fst:from:add:len
gen_0':nil:s:cons:fst:from:add:len2_0 :: Nat → 0':nil:s:cons:fst:from:add:len
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
mark,
a__fromThey will be analysed ascendingly in the following order:
mark = a__from
(8) Obligation:
TRS:
Rules:
a__fst(
0',
Z) →
nila__fst(
s(
X),
cons(
Y,
Z)) →
cons(
mark(
Y),
fst(
X,
Z))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__add(
0',
X) →
mark(
X)
a__add(
s(
X),
Y) →
s(
add(
X,
Y))
a__len(
nil) →
0'a__len(
cons(
X,
Z)) →
s(
len(
Z))
mark(
fst(
X1,
X2)) →
a__fst(
mark(
X1),
mark(
X2))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
add(
X1,
X2)) →
a__add(
mark(
X1),
mark(
X2))
mark(
len(
X)) →
a__len(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
a__fst(
X1,
X2) →
fst(
X1,
X2)
a__from(
X) →
from(
X)
a__add(
X1,
X2) →
add(
X1,
X2)
a__len(
X) →
len(
X)
Types:
a__fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
0' :: 0':nil:s:cons:fst:from:add:len
nil :: 0':nil:s:cons:fst:from:add:len
s :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
cons :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
mark :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
hole_0':nil:s:cons:fst:from:add:len1_0 :: 0':nil:s:cons:fst:from:add:len
gen_0':nil:s:cons:fst:from:add:len2_0 :: Nat → 0':nil:s:cons:fst:from:add:len
Generator Equations:
gen_0':nil:s:cons:fst:from:add:len2_0(0) ⇔ 0'
gen_0':nil:s:cons:fst:from:add:len2_0(+(x, 1)) ⇔ s(gen_0':nil:s:cons:fst:from:add:len2_0(x))
The following defined symbols remain to be analysed:
a__from, mark
They will be analysed ascendingly in the following order:
mark = a__from
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__from.
(10) Obligation:
TRS:
Rules:
a__fst(
0',
Z) →
nila__fst(
s(
X),
cons(
Y,
Z)) →
cons(
mark(
Y),
fst(
X,
Z))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__add(
0',
X) →
mark(
X)
a__add(
s(
X),
Y) →
s(
add(
X,
Y))
a__len(
nil) →
0'a__len(
cons(
X,
Z)) →
s(
len(
Z))
mark(
fst(
X1,
X2)) →
a__fst(
mark(
X1),
mark(
X2))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
add(
X1,
X2)) →
a__add(
mark(
X1),
mark(
X2))
mark(
len(
X)) →
a__len(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
a__fst(
X1,
X2) →
fst(
X1,
X2)
a__from(
X) →
from(
X)
a__add(
X1,
X2) →
add(
X1,
X2)
a__len(
X) →
len(
X)
Types:
a__fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
0' :: 0':nil:s:cons:fst:from:add:len
nil :: 0':nil:s:cons:fst:from:add:len
s :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
cons :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
mark :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
hole_0':nil:s:cons:fst:from:add:len1_0 :: 0':nil:s:cons:fst:from:add:len
gen_0':nil:s:cons:fst:from:add:len2_0 :: Nat → 0':nil:s:cons:fst:from:add:len
Generator Equations:
gen_0':nil:s:cons:fst:from:add:len2_0(0) ⇔ 0'
gen_0':nil:s:cons:fst:from:add:len2_0(+(x, 1)) ⇔ s(gen_0':nil:s:cons:fst:from:add:len2_0(x))
The following defined symbols remain to be analysed:
mark
They will be analysed ascendingly in the following order:
mark = a__from
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(12) Obligation:
TRS:
Rules:
a__fst(
0',
Z) →
nila__fst(
s(
X),
cons(
Y,
Z)) →
cons(
mark(
Y),
fst(
X,
Z))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__add(
0',
X) →
mark(
X)
a__add(
s(
X),
Y) →
s(
add(
X,
Y))
a__len(
nil) →
0'a__len(
cons(
X,
Z)) →
s(
len(
Z))
mark(
fst(
X1,
X2)) →
a__fst(
mark(
X1),
mark(
X2))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
add(
X1,
X2)) →
a__add(
mark(
X1),
mark(
X2))
mark(
len(
X)) →
a__len(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
a__fst(
X1,
X2) →
fst(
X1,
X2)
a__from(
X) →
from(
X)
a__add(
X1,
X2) →
add(
X1,
X2)
a__len(
X) →
len(
X)
Types:
a__fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
0' :: 0':nil:s:cons:fst:from:add:len
nil :: 0':nil:s:cons:fst:from:add:len
s :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
cons :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
mark :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
fst :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
from :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
add :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
a__len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
len :: 0':nil:s:cons:fst:from:add:len → 0':nil:s:cons:fst:from:add:len
hole_0':nil:s:cons:fst:from:add:len1_0 :: 0':nil:s:cons:fst:from:add:len
gen_0':nil:s:cons:fst:from:add:len2_0 :: Nat → 0':nil:s:cons:fst:from:add:len
Generator Equations:
gen_0':nil:s:cons:fst:from:add:len2_0(0) ⇔ 0'
gen_0':nil:s:cons:fst:from:add:len2_0(+(x, 1)) ⇔ s(gen_0':nil:s:cons:fst:from:add:len2_0(x))
No more defined symbols left to analyse.